/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.transl;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collections;
import java.util.HashSet;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.TreeMap;

import alloy.ast.ASTDepthFirstReturnVisitor;
import alloy.ast.DeclIter;
import alloy.ast.LeafExpr;
import alloy.ast.LeafId;
import alloy.ast.Node;
import alloy.ast.VarCreator;
import alloy.ast.Variable;
import alloy.ast.VariableExpr;

/** For each {@link Node}, computes the list of quantified variables
    on which this node depends, i.e. variables actually mentioned at some leaves
    of the AST subtree rooted at the node.  Used for displaying, in the
    {@link SwingASTVisitor Alloy Evaluator}, the value(s) of this {@link Node}
    for a given Alloy instance -- one value for each combination of
    assignments to quantified variables on which this node depends.  Note that
    a {@link VarCreator} does <em>not</em> depend on the variables it defines.
    The set of variables on which a node depends is a subset of the set of
    variables defined higher up in the AST.
    <p>
    This visitor is called on a completely desugared AST; it does not modify
    the AST -- it only gathers information, which is currently used only
    by the GUI, specifically, by the Alloy Evaluator.  See {@link alloy.gui.SwingASTVisitor}.
    <p>
    The {@link #visit} methods return the {@link List} of {@link LeafId}s of quantified
    {@link Variable}s on which the visited {@link Node} depends.  The list is in the order
    of declaration from root of the AST. */
public class VariableUsageVisitor extends ASTDepthFirstReturnVisitor {
    /** {@link Map} from {@link Node} to {@link List} of {@link LeafId}s of quantified
	{@link Variable}s on which it depends.  The visitor constructs this map as
	it traverses the AST, and this map can afterwards be requested by
	calling {@link #getNode2UsedVarIds}. */
    private Map /* Node->List[LeafId] */ _node2vars = new TreeMap();

    /** {@link List} of {@link LeafId}s of quantified {@link Variable}s declared
	from the root of the AST through the current node.  The list of variables
	on which the current node depends will be a <em>sublist</em> of this list. */
    private List _declaredVarIds = new ArrayList();

      /////////////
     // Methods //
    /////////////

    public Object visit(VariableExpr variableExpr_) {
	_node2vars.put(variableExpr_,
		       variableExpr_.isQuantified ?
		       Arrays.asList(new LeafId[]{variableExpr_.getLeafId()}) :
		       Collections.EMPTY_LIST);
	return variableExpr_.isQuantified ?
	    Collections.singleton(variableExpr_.getLeafId()) :
	    Collections.EMPTY_SET;
    }
    
    public Object visit(Node node_) {
	List varsDeclaredHere = new ArrayList();
	VarCreator varCreator = (node_ instanceof VarCreator) ? (VarCreator)node_ : null;

	if (varCreator!=null) {
	    for (DeclIter declIter = new DeclIter(varCreator); declIter.hasNext();) {
		declIter.next();  // returns a Variable, but we need the LeafId
		varsDeclaredHere.add(declIter.getLeafId());
	    }
	}
	
	Set varsUsedHere = new HashSet();
	if (!(node_ instanceof LeafExpr)) {
	    Iterator childIter = (varCreator==null) ? node_.getChildren() :
		Collections.singleton(varCreator.getBody()).iterator();

	    _declaredVarIds.addAll(varsDeclaredHere);

	    while(childIter.hasNext()) {
		Node child = (Node)childIter.next();
		varsUsedHere.addAll((Set)child.applyReturnVisitor(this));
	    }

	    _declaredVarIds.removeAll(varsDeclaredHere);
	}

	List varsOnWhichThisDepends = new ArrayList(_declaredVarIds);
	varsOnWhichThisDepends.retainAll(varsUsedHere);
	
	_node2vars.put(node_, varsOnWhichThisDepends);
	return varsUsedHere;
    }

    /** Return a {@link Map} from {@link Node} to the {@link List} of {@link LeafId}s of quantified {@link Variable}s
	on which the {@link Node} depends.  The list is in order of declaration from root of the AST.
	Called after the visitor has visited the entire AST. */
    public Map getNode2UsedVarIds() { return _node2vars; }

    /** Returns a {@link List} of {@link LeafId}s of the quantified {@link Variable}s
	encountered by this visitor. */
    public List getAllVarIds () {
	ArrayList varList = new ArrayList ();
	
	Iterator nodeIter = _node2vars.entrySet().iterator();
	while (nodeIter.hasNext()) {
	    List leafIds = (List)((Map.Entry)nodeIter.next()).getValue();

	    Iterator leafIdsIter = leafIds.iterator();
	    while (leafIdsIter.hasNext()) {
		LeafId leafId = (LeafId)leafIdsIter.next();

		if (! varList.contains (leafId))
		    varList.add (leafId);
	    }
	}

	return varList;
    }
	    

}

